Nuprl Lemma : ideal_wf
6,26
postcript
pdf
r
:CRng{i}. Ideal(
r
){i}
Type{i'}
latex
Definitions
x
:
A
.
B
(
x
)
,
t
T
,
Ideal(
r
){i}
,
Prop
,
CRng
,
Rng
Lemmas
rng
car
wf
,
ideal
p
wf
,
crng
wf
origin
r:CRng{i}. Ideal(r){i} 
Type{i'} r:CRng{i}. Ideal(r){i} Type{i'} x:A. B(x) T